《Android permissions unleashed》
来源：CSF 2015
关键词：定理证明器，Android权限模型，策略
摘要：
本文利用定力证明器为Android权限建模，将组件的权限定制成策略集合，提出了两个概念：一个是组件栈（Component stack），由frame组成,而frame F = { C, P, Φ }，其中， C为component，P为权限集，Φ为策略集。第二个是系统配置，由组件栈组成，Σ = [S1; S2; . . .]；针对frame，stack和configuration制了相应的策略范围direct,local和global；将example中的权限与上述结合，构建了权限、组件和策略的逻辑表达。